/* Complex Train-Gate system
	CLOSED LOOP BEHAVIOUR:
	ENV:
	Trains move one way on a railway line that 
	intersects with a road.
	There is a traffic light that causes trains 
	to stop as they approach a level-crossing.
	The gate must be down when the trains cross, 
	and up otherwise.
	REQ-1: [](trainOn -> gateDown)
	CHALLENGE: Describe SPEC so that ENV && SPEC ==> REQ
*/
#define trainAway sT == away
#define trainNear sT == near
#define trainOn sT == on
#define trainExited sT == exited
#define gateUp sG == up
#define gateDown sG == down
#define lightRed sL == red
#define lightGreen sL == green
#define bothAreOn sL == bothOn
/* The following should hold but does not
	[](trainOn -> gateDown)
	[](trainOff -> gateUp)
	[](trainOn -> lightGreen) FAILS

    []( trainExited -> 
      <>(gateUp && lightRed && trainAway))
*/

/* state of Train*/
mtype = {away, near, on, exited};
mtype sT = away;

/* state of Gate*/
mtype = {up, down, moving};
mtype sG = up;

/* state of Light*/
mtype = {green, red, bothOn, bothOff};
mtype sL = red;

mtype time = 0;
 
/* signal Gate to go up or down */
bool dPulse = false;

/* signal Light to go red or green */
bool rPulse = false; bool gPulse = false;

/* ENVIRONMENT = TRAIN || GATE || LIGHT || TIME*/

/*
   in: dPulse
   out: sG
*/
proctype GATE()
{
	   do
		//::  d_step {(dPulse && sG == down)  -> sG = moving};
		::  d_step {(dPulse && sG == moving) -> sG = down};
	    ::  d_step {(dPulse && sG == up) -> sG = moving};
        ::  d_step {(!dPulse && sG == moving) -> sG = up};
		::  d_step {(!dPulse && sG == down)  -> sG = moving};
       od
}

/*
   in: sL
   out: sT
*/
proctype TRAIN()
{
       do
	    ::  d_step {(sT == away) -> sT = away};
		::  d_step {(sT == away) -> sT = near};
		::  d_step {(sT == on) -> sT = exited};
		::  d_step {(sT == exited && time == 2) -> sT = away; time == 0};
		::  d_step {(sT == near && sL == green) -> sT = on};
		//::  d_step {(sT == near && sL == red) -> sT == near};

		// when train exited or away, guard needs '&& sG == up && sL == red'
		// to take into account that gate and light change faster than
		// new train comes
       od
}

/*
   in: gPulse; rPulse;
   out: sL
*/
proctype LIGHT()
{  //do I need a "changing" state? or also, do I need to have sL on the LHS?
       do
	    ::  d_step {(gPulse && !rPulse) -> sL = green};
		::  d_step {(gPulse && rPulse) -> sL = bothOn};
		::  d_step {(!gPulse && rPulse) -> sL = red};
		::  d_step {(!gPulse && !rPulse) -> sL = bothOff}; 
        
        /*
		::  d_step {(gPulse && rPulse && lightGreen) -> sL = bothOn; time = 1};
		::  d_step {(!gPulse && rPulse && lightGreen) -> sL = red; time = 1};
		::  d_step {(!gPulse && !rPulse && lightGreen) -> sL = bothOff; time = 1};
		
		::  d_step {(gPulse && !rPulse && lightRed) -> sL = green; time = 1};
		::  d_step {(gPulse && rPulse && lightRed) -> sL = bothOn; time = 1};
		::  d_step {(!gPulse && !rPulse && lightRed) -> sL = bothOff; time = 1};

		
		::  d_step {(gPulse && !rPulse && (sL == bothOn)) -> sL = green; time = 1};
		::  d_step {(!gPulse && rPulse && (sL == bothOn)) -> sL = red; time = 1};
		::  d_step {(!gPulse && !rPulse && (sL == bothOn)) -> sL = bothOff; time = 1};

		
		::  d_step {(gPulse && !rPulse && (sL == bothOff)) -> sL = green; time = 1};
		::  d_step {(gPulse && rPulse && (sL == bothOff)) -> sL = bothOn; time = 1};
		::  d_step {(!gPulse && rPulse && (sL == bothOff)) -> sL = red; time = 1};
	    */
	   od
}

/* 
*/

proctype TIME()
{
	  do	
		:: d_step {(time == 2) -> time = 0};
	  od
}

/* SPECIFICATION of machine under construction
	in: sT, SG 
	out: dPulse, sL 
*/
proctype MACHINE()
/* Version in which MACHINE controls sL via gPulse and rPulse*/

{
	do
	//prof doesn't have this first one
	//:: d_step{(trainExited && gateUp) -> 
	//			dPulse = false; gPulse = false; rPulse = true}
	:: d_step{(trainExited && gateDown) -> 
				dPulse = false; gPulse = false; rPulse = true}
	:: d_step{(trainNear && gateUp) -> 
				dPulse = true; gPulse = false; rPulse = true}
	:: d_step{(trainNear && gateDown) -> 
				dPulse = true; gPulse = true; rPulse = false}
	:: d_step{(trainOn && gateDown) -> 
				dPulse = true; gPulse = true; rPulse = false}
	od
}

init
{	
	d_step{sT = away; sG = up; sL = red; gPulse = false; 
			rPulse = true; dPulse = false};
	atomic{run GATE(); run LIGHT(); run TRAIN(); run MACHINE();}
}
